$\forall$${\it ds}$:(Id$\rightarrow$Type), ${\it da}$:(Id$\rightarrow$Knd$\rightarrow$Type), $A$:Type, $X$:Interface(${\it ds}$;${\it da}$;$A$), ${\it es}$:ES.
\\[0ex]es{-}decl(${\it es}$;${\it ds}$;${\it da}$) $\Rightarrow$ ([[$X$]] $\in$ AbsInterface($A$))